(declare-sort S0 0)

(declare-sort S1 0)

(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(assert (exists ((q0 Bool) (q1 Bool)) v4))
(declare-const v6 Bool)
(declare-const _32-0 (_ BitVec 32))
(assert (exists ((q2 Bool) (q3 Bool)) (not (distinct q2 q3 v6 v4 q2 v1 v0 v0))))
(declare-const _19-0 (_ BitVec 19))
(assert (exists ((q4 (_ BitVec 9)) (q5 (_ BitVec 9))) (not (distinct #b110101010 q4 q5 q5))))
(declare-const v7 Bool)
(declare-const v8 Bool)
(assert (not (exists ((q6 (_ BitVec 32))) (not (= q6 (bvsmod _32-0 _32-0) q6 (bvsmod _32-0 _32-0) (bvsmod _32-0 _32-0))))))
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(assert (not (forall ((q7 (_ BitVec 9)) (q8 (_ BitVec 9)) (q9 Bool) (q10 (_ BitVec 32))) (or (= q10 _32-0 q10 q10 q10) (and v8 q9) (bvule #b110101010 q8)))))
(declare-const v14 Bool)
(assert (not (exists ((q11 (_ BitVec 8)) (q12 (_ BitVec 19)) (q13 S1)) (=> (bvuge q12 q12) (distinct #b01001100 q11 q11 q11)))))
(check-sat)
